din(der(plus(X, Y))) → u21(din(der(X)), X, Y)
u21(dout(DX), X, Y) → u22(din(der(Y)), X, Y, DX)
u22(dout(DY), X, Y, DX) → dout(plus(DX, DY))
din(der(times(X, Y))) → u31(din(der(X)), X, Y)
u31(dout(DX), X, Y) → u32(din(der(Y)), X, Y, DX)
u32(dout(DY), X, Y, DX) → dout(plus(times(X, DY), times(Y, DX)))
din(der(der(X))) → u41(din(der(X)), X)
u41(dout(DX), X) → u42(din(der(DX)), X, DX)
u42(dout(DDX), X, DX) → dout(DDX)
↳ QTRS
↳ DependencyPairsProof
din(der(plus(X, Y))) → u21(din(der(X)), X, Y)
u21(dout(DX), X, Y) → u22(din(der(Y)), X, Y, DX)
u22(dout(DY), X, Y, DX) → dout(plus(DX, DY))
din(der(times(X, Y))) → u31(din(der(X)), X, Y)
u31(dout(DX), X, Y) → u32(din(der(Y)), X, Y, DX)
u32(dout(DY), X, Y, DX) → dout(plus(times(X, DY), times(Y, DX)))
din(der(der(X))) → u41(din(der(X)), X)
u41(dout(DX), X) → u42(din(der(DX)), X, DX)
u42(dout(DDX), X, DX) → dout(DDX)
DIN(der(times(X, Y))) → U31(din(der(X)), X, Y)
DIN(der(times(X, Y))) → DIN(der(X))
U41(dout(DX), X) → U42(din(der(DX)), X, DX)
DIN(der(der(X))) → U41(din(der(X)), X)
U31(dout(DX), X, Y) → U32(din(der(Y)), X, Y, DX)
U21(dout(DX), X, Y) → U22(din(der(Y)), X, Y, DX)
U41(dout(DX), X) → DIN(der(DX))
DIN(der(plus(X, Y))) → DIN(der(X))
U21(dout(DX), X, Y) → DIN(der(Y))
DIN(der(plus(X, Y))) → U21(din(der(X)), X, Y)
DIN(der(der(X))) → DIN(der(X))
U31(dout(DX), X, Y) → DIN(der(Y))
din(der(plus(X, Y))) → u21(din(der(X)), X, Y)
u21(dout(DX), X, Y) → u22(din(der(Y)), X, Y, DX)
u22(dout(DY), X, Y, DX) → dout(plus(DX, DY))
din(der(times(X, Y))) → u31(din(der(X)), X, Y)
u31(dout(DX), X, Y) → u32(din(der(Y)), X, Y, DX)
u32(dout(DY), X, Y, DX) → dout(plus(times(X, DY), times(Y, DX)))
din(der(der(X))) → u41(din(der(X)), X)
u41(dout(DX), X) → u42(din(der(DX)), X, DX)
u42(dout(DDX), X, DX) → dout(DDX)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
DIN(der(times(X, Y))) → U31(din(der(X)), X, Y)
DIN(der(times(X, Y))) → DIN(der(X))
U41(dout(DX), X) → U42(din(der(DX)), X, DX)
DIN(der(der(X))) → U41(din(der(X)), X)
U31(dout(DX), X, Y) → U32(din(der(Y)), X, Y, DX)
U21(dout(DX), X, Y) → U22(din(der(Y)), X, Y, DX)
U41(dout(DX), X) → DIN(der(DX))
DIN(der(plus(X, Y))) → DIN(der(X))
U21(dout(DX), X, Y) → DIN(der(Y))
DIN(der(plus(X, Y))) → U21(din(der(X)), X, Y)
DIN(der(der(X))) → DIN(der(X))
U31(dout(DX), X, Y) → DIN(der(Y))
din(der(plus(X, Y))) → u21(din(der(X)), X, Y)
u21(dout(DX), X, Y) → u22(din(der(Y)), X, Y, DX)
u22(dout(DY), X, Y, DX) → dout(plus(DX, DY))
din(der(times(X, Y))) → u31(din(der(X)), X, Y)
u31(dout(DX), X, Y) → u32(din(der(Y)), X, Y, DX)
u32(dout(DY), X, Y, DX) → dout(plus(times(X, DY), times(Y, DX)))
din(der(der(X))) → u41(din(der(X)), X)
u41(dout(DX), X) → u42(din(der(DX)), X, DX)
u42(dout(DDX), X, DX) → dout(DDX)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
DIN(der(times(X, Y))) → U31(din(der(X)), X, Y)
DIN(der(times(X, Y))) → DIN(der(X))
DIN(der(der(X))) → U41(din(der(X)), X)
U41(dout(DX), X) → DIN(der(DX))
DIN(der(plus(X, Y))) → DIN(der(X))
DIN(der(plus(X, Y))) → U21(din(der(X)), X, Y)
U21(dout(DX), X, Y) → DIN(der(Y))
DIN(der(der(X))) → DIN(der(X))
U31(dout(DX), X, Y) → DIN(der(Y))
din(der(plus(X, Y))) → u21(din(der(X)), X, Y)
u21(dout(DX), X, Y) → u22(din(der(Y)), X, Y, DX)
u22(dout(DY), X, Y, DX) → dout(plus(DX, DY))
din(der(times(X, Y))) → u31(din(der(X)), X, Y)
u31(dout(DX), X, Y) → u32(din(der(Y)), X, Y, DX)
u32(dout(DY), X, Y, DX) → dout(plus(times(X, DY), times(Y, DX)))
din(der(der(X))) → u41(din(der(X)), X)
u41(dout(DX), X) → u42(din(der(DX)), X, DX)
u42(dout(DDX), X, DX) → dout(DDX)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U31(dout(DX), X, Y) → DIN(der(Y))
Used ordering: Polynomial interpretation [25,35]:
DIN(der(times(X, Y))) → U31(din(der(X)), X, Y)
DIN(der(times(X, Y))) → DIN(der(X))
DIN(der(der(X))) → U41(din(der(X)), X)
U41(dout(DX), X) → DIN(der(DX))
DIN(der(plus(X, Y))) → DIN(der(X))
DIN(der(plus(X, Y))) → U21(din(der(X)), X, Y)
U21(dout(DX), X, Y) → DIN(der(Y))
DIN(der(der(X))) → DIN(der(X))
The value of delta used in the strict ordering is 1/8.
POL(plus(x1, x2)) = 0
POL(u32(x1, x2, x3, x4)) = x_1
POL(u42(x1, x2, x3)) = 1/2 + (1/2)x_1
POL(u31(x1, x2, x3)) = 0
POL(DIN(x1)) = 0
POL(der(x1)) = 0
POL(U31(x1, x2, x3)) = (1/2)x_1
POL(din(x1)) = 0
POL(U41(x1, x2)) = 0
POL(times(x1, x2)) = 1/4 + (4)x_1
POL(u22(x1, x2, x3, x4)) = 1/4
POL(u41(x1, x2)) = (9/4)x_1
POL(dout(x1)) = 1/4
POL(U21(x1, x2, x3)) = 0
POL(u21(x1, x2, x3)) = (5/4)x_1
din(der(plus(X, Y))) → u21(din(der(X)), X, Y)
u21(dout(DX), X, Y) → u22(din(der(Y)), X, Y, DX)
u22(dout(DY), X, Y, DX) → dout(plus(DX, DY))
u31(dout(DX), X, Y) → u32(din(der(Y)), X, Y, DX)
din(der(times(X, Y))) → u31(din(der(X)), X, Y)
din(der(der(X))) → u41(din(der(X)), X)
u32(dout(DY), X, Y, DX) → dout(plus(times(X, DY), times(Y, DX)))
u42(dout(DDX), X, DX) → dout(DDX)
u41(dout(DX), X) → u42(din(der(DX)), X, DX)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
DIN(der(times(X, Y))) → U31(din(der(X)), X, Y)
DIN(der(times(X, Y))) → DIN(der(X))
DIN(der(der(X))) → U41(din(der(X)), X)
U41(dout(DX), X) → DIN(der(DX))
DIN(der(plus(X, Y))) → DIN(der(X))
U21(dout(DX), X, Y) → DIN(der(Y))
DIN(der(plus(X, Y))) → U21(din(der(X)), X, Y)
DIN(der(der(X))) → DIN(der(X))
din(der(plus(X, Y))) → u21(din(der(X)), X, Y)
u21(dout(DX), X, Y) → u22(din(der(Y)), X, Y, DX)
u22(dout(DY), X, Y, DX) → dout(plus(DX, DY))
din(der(times(X, Y))) → u31(din(der(X)), X, Y)
u31(dout(DX), X, Y) → u32(din(der(Y)), X, Y, DX)
u32(dout(DY), X, Y, DX) → dout(plus(times(X, DY), times(Y, DX)))
din(der(der(X))) → u41(din(der(X)), X)
u41(dout(DX), X) → u42(din(der(DX)), X, DX)
u42(dout(DDX), X, DX) → dout(DDX)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
DIN(der(times(X, Y))) → DIN(der(X))
DIN(der(der(X))) → U41(din(der(X)), X)
U41(dout(DX), X) → DIN(der(DX))
DIN(der(plus(X, Y))) → DIN(der(X))
U21(dout(DX), X, Y) → DIN(der(Y))
DIN(der(plus(X, Y))) → U21(din(der(X)), X, Y)
DIN(der(der(X))) → DIN(der(X))
din(der(plus(X, Y))) → u21(din(der(X)), X, Y)
u21(dout(DX), X, Y) → u22(din(der(Y)), X, Y, DX)
u22(dout(DY), X, Y, DX) → dout(plus(DX, DY))
din(der(times(X, Y))) → u31(din(der(X)), X, Y)
u31(dout(DX), X, Y) → u32(din(der(Y)), X, Y, DX)
u32(dout(DY), X, Y, DX) → dout(plus(times(X, DY), times(Y, DX)))
din(der(der(X))) → u41(din(der(X)), X)
u41(dout(DX), X) → u42(din(der(DX)), X, DX)
u42(dout(DDX), X, DX) → dout(DDX)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U41(dout(DX), X) → DIN(der(DX))
Used ordering: Polynomial interpretation [25,35]:
DIN(der(times(X, Y))) → DIN(der(X))
DIN(der(der(X))) → U41(din(der(X)), X)
DIN(der(plus(X, Y))) → DIN(der(X))
U21(dout(DX), X, Y) → DIN(der(Y))
DIN(der(plus(X, Y))) → U21(din(der(X)), X, Y)
DIN(der(der(X))) → DIN(der(X))
The value of delta used in the strict ordering is 1.
POL(plus(x1, x2)) = 3/4
POL(u32(x1, x2, x3, x4)) = 1 + (1/4)x_1
POL(u42(x1, x2, x3)) = 1
POL(u31(x1, x2, x3)) = (4)x_1
POL(DIN(x1)) = 0
POL(der(x1)) = 0
POL(din(x1)) = (2)x_1
POL(U41(x1, x2)) = (4)x_1
POL(times(x1, x2)) = (1/4)x_1
POL(u22(x1, x2, x3, x4)) = 1/4
POL(u41(x1, x2)) = (4)x_1
POL(dout(x1)) = 1/4
POL(U21(x1, x2, x3)) = 0
POL(u21(x1, x2, x3)) = (4)x_1
din(der(plus(X, Y))) → u21(din(der(X)), X, Y)
u21(dout(DX), X, Y) → u22(din(der(Y)), X, Y, DX)
u22(dout(DY), X, Y, DX) → dout(plus(DX, DY))
u31(dout(DX), X, Y) → u32(din(der(Y)), X, Y, DX)
din(der(times(X, Y))) → u31(din(der(X)), X, Y)
din(der(der(X))) → u41(din(der(X)), X)
u32(dout(DY), X, Y, DX) → dout(plus(times(X, DY), times(Y, DX)))
u42(dout(DDX), X, DX) → dout(DDX)
u41(dout(DX), X) → u42(din(der(DX)), X, DX)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
DIN(der(times(X, Y))) → DIN(der(X))
DIN(der(der(X))) → U41(din(der(X)), X)
DIN(der(plus(X, Y))) → DIN(der(X))
DIN(der(plus(X, Y))) → U21(din(der(X)), X, Y)
U21(dout(DX), X, Y) → DIN(der(Y))
DIN(der(der(X))) → DIN(der(X))
din(der(plus(X, Y))) → u21(din(der(X)), X, Y)
u21(dout(DX), X, Y) → u22(din(der(Y)), X, Y, DX)
u22(dout(DY), X, Y, DX) → dout(plus(DX, DY))
din(der(times(X, Y))) → u31(din(der(X)), X, Y)
u31(dout(DX), X, Y) → u32(din(der(Y)), X, Y, DX)
u32(dout(DY), X, Y, DX) → dout(plus(times(X, DY), times(Y, DX)))
din(der(der(X))) → u41(din(der(X)), X)
u41(dout(DX), X) → u42(din(der(DX)), X, DX)
u42(dout(DDX), X, DX) → dout(DDX)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
DIN(der(times(X, Y))) → DIN(der(X))
DIN(der(plus(X, Y))) → DIN(der(X))
U21(dout(DX), X, Y) → DIN(der(Y))
DIN(der(plus(X, Y))) → U21(din(der(X)), X, Y)
DIN(der(der(X))) → DIN(der(X))
din(der(plus(X, Y))) → u21(din(der(X)), X, Y)
u21(dout(DX), X, Y) → u22(din(der(Y)), X, Y, DX)
u22(dout(DY), X, Y, DX) → dout(plus(DX, DY))
din(der(times(X, Y))) → u31(din(der(X)), X, Y)
u31(dout(DX), X, Y) → u32(din(der(Y)), X, Y, DX)
u32(dout(DY), X, Y, DX) → dout(plus(times(X, DY), times(Y, DX)))
din(der(der(X))) → u41(din(der(X)), X)
u41(dout(DX), X) → u42(din(der(DX)), X, DX)
u42(dout(DDX), X, DX) → dout(DDX)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DIN(der(times(X, Y))) → DIN(der(X))
DIN(der(plus(X, Y))) → DIN(der(X))
DIN(der(plus(X, Y))) → U21(din(der(X)), X, Y)
Used ordering: Polynomial interpretation [25,35]:
U21(dout(DX), X, Y) → DIN(der(Y))
DIN(der(der(X))) → DIN(der(X))
The value of delta used in the strict ordering is 12.
POL(plus(x1, x2)) = 3 + (2)x_1 + (4)x_2
POL(u32(x1, x2, x3, x4)) = 1 + (3)x_2 + (3)x_3 + (3)x_4
POL(u42(x1, x2, x3)) = 3 + (3)x_1 + (3)x_2 + (3)x_3
POL(u31(x1, x2, x3)) = 3 + (3)x_2 + (2)x_3
POL(DIN(x1)) = 4 + x_1
POL(der(x1)) = (4)x_1
POL(din(x1)) = 1 + (4)x_1
POL(times(x1, x2)) = 4 + x_1
POL(u22(x1, x2, x3, x4)) = 3 + (3)x_2 + (3)x_3 + (4)x_4
POL(u41(x1, x2)) = 3 + (3)x_2
POL(dout(x1)) = 2 + x_1
POL(U21(x1, x2, x3)) = 4 + (3)x_2 + (4)x_3
POL(u21(x1, x2, x3)) = 3 + (3)x_1 + (2)x_2 + (2)x_3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
U21(dout(DX), X, Y) → DIN(der(Y))
DIN(der(der(X))) → DIN(der(X))
din(der(plus(X, Y))) → u21(din(der(X)), X, Y)
u21(dout(DX), X, Y) → u22(din(der(Y)), X, Y, DX)
u22(dout(DY), X, Y, DX) → dout(plus(DX, DY))
din(der(times(X, Y))) → u31(din(der(X)), X, Y)
u31(dout(DX), X, Y) → u32(din(der(Y)), X, Y, DX)
u32(dout(DY), X, Y, DX) → dout(plus(times(X, DY), times(Y, DX)))
din(der(der(X))) → u41(din(der(X)), X)
u41(dout(DX), X) → u42(din(der(DX)), X, DX)
u42(dout(DDX), X, DX) → dout(DDX)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
DIN(der(der(X))) → DIN(der(X))
din(der(plus(X, Y))) → u21(din(der(X)), X, Y)
u21(dout(DX), X, Y) → u22(din(der(Y)), X, Y, DX)
u22(dout(DY), X, Y, DX) → dout(plus(DX, DY))
din(der(times(X, Y))) → u31(din(der(X)), X, Y)
u31(dout(DX), X, Y) → u32(din(der(Y)), X, Y, DX)
u32(dout(DY), X, Y, DX) → dout(plus(times(X, DY), times(Y, DX)))
din(der(der(X))) → u41(din(der(X)), X)
u41(dout(DX), X) → u42(din(der(DX)), X, DX)
u42(dout(DDX), X, DX) → dout(DDX)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DIN(der(der(X))) → DIN(der(X))
The value of delta used in the strict ordering is 16.
POL(DIN(x1)) = (4)x_1
POL(der(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
din(der(plus(X, Y))) → u21(din(der(X)), X, Y)
u21(dout(DX), X, Y) → u22(din(der(Y)), X, Y, DX)
u22(dout(DY), X, Y, DX) → dout(plus(DX, DY))
din(der(times(X, Y))) → u31(din(der(X)), X, Y)
u31(dout(DX), X, Y) → u32(din(der(Y)), X, Y, DX)
u32(dout(DY), X, Y, DX) → dout(plus(times(X, DY), times(Y, DX)))
din(der(der(X))) → u41(din(der(X)), X)
u41(dout(DX), X) → u42(din(der(DX)), X, DX)
u42(dout(DDX), X, DX) → dout(DDX)